R:Realizer, y, i:Id. read-restricted(R; i; y)   

latex

Definitions	Realizer, t  T, Id, Knd, type List, x:A. B(x), a = b, p  q, IdLnk, false, Type, x. t(x), a:A fp B(a), Prop, x:AB(x), State(ds), DeclaredType(ds;x), x:AB(x), , p  q, x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind, read-restricted(R; i; y)
Lemmas	es realizer ind wf, bor wf, bool wf, decl-type wf, decl-state wf, fpf wf, bfalse wf, IdLnk wf, band wf, eq id wf, Knd wf, Id wf, es realizer wf